gnome-shell-build-setup.sh: add a note about removing install directory

If the user relocates from ~/gnome-shell to ~/gnome, they need to
remove the install directory or left-over paths will cause problems.

diff --git a/tools/build/gnome-shell-build-setup.sh b/tools/build/gnome-shell-build-setup.sh
index d546bb4acabfd897f2e0fecc9c81b17688066fcf..fd511aa1fa9660cdae768998ad311a179dfcd638 100755 (executable)
--- a/tools/build/gnome-shell-build-setup.sh
+++ b/tools/build/gnome-shell-build-setup.sh
@@ -304,11 +304,13 @@ WARNING:
   The old source and install directory '$HOME/gnome-shell' exists, but
   '$HOME/gnome' doesn't. An empty $HOME/gnome will be created.
 
-  To avoid starting again from scratch you should remove the empty directory
-  and move your old '$HOME/gnome-shell' to '$HOME/gnome':
+  To avoid starting again from scratch you should remove the empty directory,
+  move your old '$HOME/gnome-shell' to '$HOME/gnome', and delete the old
+  install directory:
 
     rm -rf $HOME/gnome
     mv $HOME/gnome-shell $HOME/gnome
+    rm -rf $HOME/gnome/install
 EOF
 fi